package typechecker;

import java.util.Collections;
import java.util.Set;

/**
 * The stage of a type constructor:
 * 		S = Vars | S^ | Inf 
 * 
 * Stages of the form vNNN are inference stage variables.
 */
public class Stage {
	public static final int INFINITY_VALUE = Integer.MAX_VALUE;
	public static final Stage INFINITY = new Stage("-", Integer.MAX_VALUE){
		public String preetyPrint() {return "w"; };
		@Override
		public int getSucc() {
			return INFINITY_VALUE;
		}
		@Override
		public Stage succ() {return this;};
	};
	/* Stage variable representing a value in the NT type */
	public static final Stage NONTERM = new Stage("nt", Integer.MAX_VALUE-1){
		public String preetyPrint() {return "nt"; };
		@Override
		public int getSucc() {
			return INFINITY_VALUE-1;
		}
		@Override
		public Stage succ() {return this;};
	};
	
	public static final String TEMPLATE_VAR_NAME = "i";
	
	private String baseVar;
	private int succ;
	
	public Stage(String baseVar , int succ) {
		this.baseVar = baseVar;
		this.succ = succ;
	}
	
	public String getBaseVar() {
		return baseVar;
	}
	
	public int getSucc() {
		return succ;
	}
	
	public boolean isInfinity(){
		return this.equals(INFINITY);
	}
	
	public Stage succ(){
		return new Stage(baseVar, succ+1);
	}
	
	public String preetyPrint(){
		String ret = baseVar;
		for(int i=0; i < succ; i++)
			ret = "$" + ret;
		return ret;
	}
	
	/**
	 * Helper method. Finds a fresh variable number with respect to a set of used variables
	 * @param v The set of used variables
	 * @return The number of the fresh variable
	 */
	public static int freshStageVar(Set<Integer> v){
		return (v.isEmpty())? 0 : Collections.max(v)+1;
	}
	
	public static Stage inferenceStageVariable(int i){
		return new Stage("v"+i, 0);
	}
	
	public int getIndexOfInferenceVar(){
		if(baseVar.startsWith("v")){
			return Integer.parseInt(baseVar.substring(1));
		}
		return -1;
	}
}
